YES 1.499
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((elem :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((elem :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) :: (Eq a, Eq b) => Either b a -> [Either b a] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (elem :: (Eq b, Eq a) => Either a b -> [Either a b] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2400), Succ(xv4001000)) → new_primPlusNat(xv2400, xv4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2400), Succ(xv4001000)) → new_primPlusNat(xv2400, xv4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, cc), cd), ce) → new_esEs(xv300, xv4000, cc, cd)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], eg), gb) → new_esEs1(xv301, xv4001, eg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(ty_@2, gg), gh)) → new_esEs(xv302, xv4002, gg, gh)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, eh), fa)) → new_esEs(xv300, xv4000, eh, fa)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, bbf), bbg), gf, bab) → new_esEs2(xv300, xv4000, bbf, bbg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(ty_Maybe, bac), bab) → new_esEs0(xv301, xv4001, bac)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(ty_[], hb)) → new_esEs1(xv302, xv4002, hb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(ty_Maybe, ha)) → new_esEs0(xv302, xv4002, ha)
new_esEs0(Just(xv300), Just(xv4000), app(ty_Maybe, dh)) → new_esEs0(xv300, xv4000, dh)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(ty_[], bad), bab) → new_esEs1(xv301, xv4001, bad)
new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, gc), gd), gb) → new_esEs2(xv30, xv400, gc, gd)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, cf)), ce), gb) → new_esEs0(xv300, xv4000, cf)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(ty_[], be)), gb) → new_esEs1(xv301, xv4001, be)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, bbd)), gf), bab), gb) → new_esEs0(xv300, xv4000, bbd)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, bbf), bbg)), gf), bab), gb) → new_esEs2(xv300, xv4000, bbf, bbg)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, eh), fa)), gb) → new_esEs(xv300, xv4000, eh, fa)
new_esEs0(Just(xv300), Just(xv4000), app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(xv300, xv4000, ed, ee, ef)
new_esEs0(Just(xv300), Just(xv4000), app(ty_[], ea)) → new_esEs1(xv300, xv4000, ea)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(ty_[], be)) → new_esEs1(xv301, xv4001, be)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xv301, xv4001, bh, ca, cb)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv30, xv400, bcd, bce)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_Either, bch), bda)) → new_esEs2(xv30, xv400, bch, bda)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(ty_@2, hh), baa)), bab), gb) → new_esEs(xv301, xv4001, hh, baa)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, fg), fh), ga)), gb) → new_esEs3(xv300, xv4000, fg, fh, ga)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, bbd), gf, bab) → new_esEs0(xv300, xv4000, bbd)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(xv301, xv4001, bb, bc)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(ty_Either, bae), baf)), bab), gb) → new_esEs2(xv301, xv4001, bae, baf)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_Maybe, dh)), gb) → new_esEs0(xv300, xv4000, dh)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, bbh), bca), bcb)), gf), bab), gb) → new_esEs3(xv300, xv4000, bbh, bca, bcb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, dc), dd), de), ce) → new_esEs3(xv300, xv4000, dc, dd, de)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_Either, eb), ec)), gb) → new_esEs2(xv300, xv4000, eb, ec)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_Either, eb), ec)) → new_esEs2(xv300, xv4000, eb, ec)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(app(ty_@3, he), hf), hg)), gb) → new_esEs3(xv302, xv4002, he, hf, hg)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, dc), dd), de)), ce), gb) → new_esEs3(xv300, xv4000, dc, dd, de)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(ty_@2, hh), baa), bab) → new_esEs(xv301, xv4001, hh, baa)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(app(ty_@3, he), hf), hg)) → new_esEs3(xv302, xv4002, he, hf, hg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(ty_[], bad)), bab), gb) → new_esEs1(xv301, xv4001, bad)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, fb)), gb) → new_esEs0(xv300, xv4000, fb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, bbb), bbc), gf, bab) → new_esEs(xv300, xv4000, bbb, bbc)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], cg), ce) → new_esEs1(xv300, xv4000, cg)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), eg) → new_esEs1(xv301, xv4001, eg)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, da), db)), ce), gb) → new_esEs2(xv300, xv4000, da, db)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(ty_Either, bae), baf), bab) → new_esEs2(xv301, xv4001, bae, baf)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], fc)) → new_esEs1(xv300, xv4000, fc)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(ty_Maybe, bac)), bab), gb) → new_esEs0(xv301, xv4001, bac)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(ty_Maybe, bd)) → new_esEs0(xv301, xv4001, bd)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_@2, df), dg)), gb) → new_esEs(xv300, xv4000, df, dg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(app(ty_@3, bag), bah), bba)), bab), gb) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, fd), ff)) → new_esEs2(xv300, xv4000, fd, ff)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(app(ty_@3, bh), ca), cb)), gb) → new_esEs3(xv301, xv4001, bh, ca, cb)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, bbb), bbc)), gf), bab), gb) → new_esEs(xv300, xv4000, bbb, bbc)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(app(ty_@3, ed), ee), ef)), gb) → new_esEs3(xv300, xv4000, ed, ee, ef)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(ty_Either, hc), hd)) → new_esEs2(xv302, xv4002, hc, hd)
new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_[], bcg)) → new_esEs1(xv30, xv400, bcg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(app(ty_@3, bag), bah), bba), bab) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_@2, df), dg)) → new_esEs(xv300, xv4000, df, dg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(ty_[], hb)), gb) → new_esEs1(xv302, xv4002, hb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, cf), ce) → new_esEs0(xv300, xv4000, cf)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, fb)) → new_esEs0(xv300, xv4000, fb)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, fd), ff)), gb) → new_esEs2(xv300, xv4000, fd, ff)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(ty_Either, bf), bg)) → new_esEs2(xv301, xv4001, bf, bg)
new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(xv300, xv4000, fg, fh, ga)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(ty_@2, gg), gh)), gb) → new_esEs(xv302, xv4002, gg, gh)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(ty_Either, hc), hd)), gb) → new_esEs2(xv302, xv4002, hc, hd)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, da), db), ce) → new_esEs2(xv300, xv4000, da, db)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], bbe), gf, bab) → new_esEs1(xv300, xv4000, bbe)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_[], fc)), gb) → new_esEs1(xv300, xv4000, fc)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, cc), cd)), ce), gb) → new_esEs(xv300, xv4000, cc, cd)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(ty_Either, bf), bg)), gb) → new_esEs2(xv301, xv4001, bf, bg)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_[], ea)), gb) → new_esEs1(xv300, xv4000, ea)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], bbe)), gf), bab), gb) → new_esEs1(xv300, xv4000, bbe)
new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_Maybe, bcf)) → new_esEs0(xv30, xv400, bcf)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv30, xv400, bdb, bdc, bdd)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(ty_Maybe, ha)), gb) → new_esEs0(xv302, xv4002, ha)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(ty_@2, bb), bc)), gb) → new_esEs(xv301, xv4001, bb, bc)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(ty_Maybe, bd)), gb) → new_esEs0(xv301, xv4001, bd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bbh), bca), bcb), gf, bab) → new_esEs3(xv300, xv4000, bbh, bca, bcb)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], cg)), ce), gb) → new_esEs1(xv300, xv4000, cg)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, eh), fa)) → new_esEs(xv300, xv4000, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, fd), ff)) → new_esEs2(xv300, xv4000, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(xv300, xv4000, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, fb)) → new_esEs0(xv300, xv4000, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xv300), Just(xv4000), app(app(ty_@2, df), dg)) → new_esEs(xv300, xv4000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv300), Just(xv4000), app(app(ty_Either, eb), ec)) → new_esEs2(xv300, xv4000, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv300), Just(xv4000), app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(xv300, xv4000, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xv300), Just(xv4000), app(ty_[], ea)) → new_esEs1(xv300, xv4000, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xv300), Just(xv4000), app(ty_Maybe, dh)) → new_esEs0(xv300, xv4000, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, cc), cd), ce) → new_esEs(xv300, xv4000, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(xv301, xv4001, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(ty_Either, bf), bg)) → new_esEs2(xv301, xv4001, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, da), db), ce) → new_esEs2(xv300, xv4000, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xv301, xv4001, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, dc), dd), de), ce) → new_esEs3(xv300, xv4000, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(ty_[], be)) → new_esEs1(xv301, xv4001, be)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], cg), ce) → new_esEs1(xv300, xv4000, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), ba, app(ty_Maybe, bd)) → new_esEs0(xv301, xv4001, bd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, cf), ce) → new_esEs0(xv300, xv4000, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, eh), fa)), gb) → new_esEs(xv300, xv4000, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv30, xv400, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(ty_@2, hh), baa)), bab), gb) → new_esEs(xv301, xv4001, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_@2, df), dg)), gb) → new_esEs(xv300, xv4000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, bbb), bbc)), gf), bab), gb) → new_esEs(xv300, xv4000, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(ty_@2, gg), gh)), gb) → new_esEs(xv302, xv4002, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, cc), cd)), ce), gb) → new_esEs(xv300, xv4000, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(ty_@2, bb), bc)), gb) → new_esEs(xv301, xv4001, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(ty_@2, gg), gh)) → new_esEs(xv302, xv4002, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(ty_@2, hh), baa), bab) → new_esEs(xv301, xv4001, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, bbb), bbc), gf, bab) → new_esEs(xv300, xv4000, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), eg) → new_esEs1(xv301, xv4001, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], fc)) → new_esEs1(xv300, xv4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, gc), gd), gb) → new_esEs2(xv30, xv400, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, bbf), bbg)), gf), bab), gb) → new_esEs2(xv300, xv4000, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_Either, bch), bda)) → new_esEs2(xv30, xv400, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(ty_Either, bae), baf)), bab), gb) → new_esEs2(xv301, xv4001, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_Either, eb), ec)), gb) → new_esEs2(xv300, xv4000, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, da), db)), ce), gb) → new_esEs2(xv300, xv4000, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, fd), ff)), gb) → new_esEs2(xv300, xv4000, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(ty_Either, hc), hd)), gb) → new_esEs2(xv302, xv4002, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(ty_Either, bf), bg)), gb) → new_esEs2(xv301, xv4001, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, bbf), bbg), gf, bab) → new_esEs2(xv300, xv4000, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(ty_Either, bae), baf), bab) → new_esEs2(xv301, xv4001, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(ty_Either, hc), hd)) → new_esEs2(xv302, xv4002, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, fg), fh), ga)), gb) → new_esEs3(xv300, xv4000, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, bbh), bca), bcb)), gf), bab), gb) → new_esEs3(xv300, xv4000, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(app(app(ty_@3, he), hf), hg)), gb) → new_esEs3(xv302, xv4002, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, dc), dd), de)), ce), gb) → new_esEs3(xv300, xv4000, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(app(app(ty_@3, bag), bah), bba)), bab), gb) → new_esEs3(xv301, xv4001, bag, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(app(app(ty_@3, bh), ca), cb)), gb) → new_esEs3(xv301, xv4001, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(app(ty_@3, ed), ee), ef)), gb) → new_esEs3(xv300, xv4000, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv30, xv400, bdb, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(app(app(ty_@3, he), hf), hg)) → new_esEs3(xv302, xv4002, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(app(app(ty_@3, bag), bah), bba), bab) → new_esEs3(xv301, xv4001, bag, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bbh), bca), bcb), gf, bab) → new_esEs3(xv300, xv4000, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], eg), gb) → new_esEs1(xv301, xv4001, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(ty_[], be)), gb) → new_esEs1(xv301, xv4001, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(ty_[], bad)), bab), gb) → new_esEs1(xv301, xv4001, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_[], bcg)) → new_esEs1(xv30, xv400, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(ty_[], hb)), gb) → new_esEs1(xv302, xv4002, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_[], fc)), gb) → new_esEs1(xv300, xv4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], bbe)), gf), bab), gb) → new_esEs1(xv300, xv4000, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_[], ea)), gb) → new_esEs1(xv300, xv4000, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], cg)), ce), gb) → new_esEs1(xv300, xv4000, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(ty_[], hb)) → new_esEs1(xv302, xv4002, hb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(ty_[], bad), bab) → new_esEs1(xv301, xv4001, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], bbe), gf, bab) → new_esEs1(xv300, xv4000, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, cf)), ce), gb) → new_esEs0(xv300, xv4000, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, bbd)), gf), bab), gb) → new_esEs0(xv300, xv4000, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_Maybe, dh)), gb) → new_esEs0(xv300, xv4000, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, fb)), gb) → new_esEs0(xv300, xv4000, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), app(ty_Maybe, bac)), bab), gb) → new_esEs0(xv301, xv4001, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_Maybe, bcf)) → new_esEs0(xv30, xv400, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, ba), app(ty_Maybe, bd)), gb) → new_esEs0(xv301, xv4001, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, ge), gf), app(ty_Maybe, ha)), gb) → new_esEs0(xv302, xv4002, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, app(ty_Maybe, bac), bab) → new_esEs0(xv301, xv4001, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), ge, gf, app(ty_Maybe, ha)) → new_esEs0(xv302, xv4002, ha)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, bbd), gf, bab) → new_esEs0(xv300, xv4000, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4